MAVLink是一种应用于无人机（UAV）与地面站（GCS）之间的轻量级通信协议，它定义了一组包括UAV状态和GCS控制命令的UAV与GCS交互的双向消息。针对MAVLink协议缺乏足够的安全机制，存在可能导致严重威胁和隐患的安全漏洞的问题，提出了一种基于MAVLink协议的UAV系统安全通信方案。首先，UAV持续交替广播连接请求。然后，GCS向UAV发送公钥，双方利用DH算法进行密钥协商计算出共享密钥，并使用AES算法对MAVLink消息包进行加密通信，完成身份认证；若UAV在规定时间内未收到GCS发送的公钥或对MAVLink消息包解密错误则主动断开连接，更新公钥后重新广播连接请求。另外，针对UAV系统存在被恶意篡改的安全问题，在启动引导时对UAV系统固件进行了自校验。最后，基于形式化验证工具UPPAAL证明了所提方案具有活性、可连接性以及连接唯一性，并对UAV PX4 1.6.0与GCSQgroundControl3.5.0的通信过程进行抓包测试。结果表明，所提的UAV系统安全通信方案能够防止在UAV与GCS通信过程中存在的恶意窃听、篡改消息、中间人攻击等恶意攻击，并且对UAV性能影响较小，较好地解决了MAVLink协议存在的安全漏洞。

面向嵌入式软件的开发工具目前正在从基于代码的传统开发环境向基于模型的开发环境发展。为此，研究了一个基于模型的嵌入式开发环境LambdaMDE，在LambdaPro的基础上集成OSATE和Simulink模型开发工具以及其他相关工具，包含了建模、仿真验证、代码生成和测试等嵌入式软件开发的全过程。符合嵌入式软件开发工具发展趋势，具备了相应的理论、技术和产品基础。

针对体系结构分析设计语言(AADL)模型的可调度性验证问题，提出了利用模型检测工具UPPAAL对其线程组件在非抢占型调度策略下的可调度性进行形式化分析和验证的方法，并实现了从AADL模型到UPPAAL中模型的模型转换工具。实验结果证明了通过UPPAAL来分析和验证AADL模型的可调度性问题的可行性。相比其他方法而言，基于形式化理论的本方法的验证结果更加精确。